---------------- MODULE run_liste_ralR1 ----------------

EXTENDS Naturals, FiniteSets, Sequences, var_raffinement

CONSTANT
    L, N, D

A == INSTANCE liste

C == INSTANCE ralR1

ASSUME (N + 1 = C!Power2[L])

Liaison(etatA, etatC) ==
  /\ \A i \in 1..Len(etatA) : etatA[i] = C!Get[i, etatC]
  /\ Len(etatA) = C!RalToInteger[etatC]

INSTANCE run_raffinement WITH ETATA <- A!ETAT, InitA <- A!Init, ContratClientA <- A!ContratClient, ContratModuleA <- A!ContratModule,
                              ETATC <- C!ETAT, InitC <- C!Init, ContratClientC <- C!ContratClient, ContratModuleC <- C!ContratModule


================================================================
